Nuprl Lemma : non-void-decl_wf
11,40
postcript
pdf
T
:Type{i},
eq
:EqDecider(
T
),
d
:
a
:
T
fp
Type{i}. non-void(
d
)
{i'}
latex
Definitions
non-void(
d
)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
x
,
y
.
t
(
x
;
y
)
,
,
b
,
x
dom(
f
)
,
Top
,
a
:
A
fp
B
(
a
)
,
x
.
t
(
x
)
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
fpf
wf
,
fpf-trivial-subtype-top
,
fpf-dom
wf
,
assert
wf
,
fpf-all
wf
origin
T:Type{i}, eq:EqDecider(T), d:a:T fp
Type{i}. non-void(d) 
{i'} T:Type{i}, eq:EqDecider(T), d:a:T fp Type{i}. non-void(d) {i'} xdom(f). v=f(x) 
P(x;v)
x,y. t(x;y)
b dom(f) B(a)x. t(x)x:A. B(x) T